Nuprl Definition : Q-R-pre-preserving 11,40

f is Q-R-pre-preserving on P == e, e':{e:E| P(e)} . (Q(f(e),f(e')))  (R(e,e')) 
latex



clarification:

Q-R-pre-preserving(es;f;P;Q;R)
== e:{e:es-E(es)| P(e)} , e':{e:es-E(es)| P(e)} . (Q(f(e),f(e')))  (R(e,e')) 
latex


Definitionsx:A. B(x), {x:A| B(x)} , E, P  Q, f(a)
FDL editor aliasesQ-R-pre-preserving

origin